#ifndef EXPRDEF_H
#define EXPRDEF_H
#include <vector>
using namespace std;

//enum QuantType {Forall, Exist};
enum PropType { LT, GT, Eq};
enum LogicType { And, Or, Imp};
enum OPType { Plus, Minus, Multi, Divide /*, Bitor, Bitand, Bitxor, Mod*/ };

struct Expr{
    virtual ~Expr(){ }
virtual bool operator==(Expr &other)=0;
};
struct IntExpr: Expr{//Integer
    int i;
    bool operator==(Expr &other);
};
/*struct SelectExpr: Expr{
    Expr* a;//name of an array
    Expr* i;//index
    bool operator==(Expr &other);
    bool IsTheSameArray(Expr &other);
};
struct StoreExpr: Expr{
    Expr *a;//name of an array
    Expr *i;//index
    Expr *e;//expersion stores a value
    //store(a, i, e)
    bool operator==(Expr &other);
};*/

struct VarExpr: Expr{//variable
    char x[256];
    bool operator==(Expr &other);
};
struct BinExpr: Expr{
    Expr *e1, *e2;
    OPType op;
    bool operator==(Expr &other);
};




struct Prop{
    virtual ~Prop(){ }
    virtual bool operator==(Prop &other)=0;
};
struct BoolProp:Prop{
    bool b;
    bool operator==(Prop &other);
};
struct NegProp:Prop{
    Prop *p;
    bool operator==(Prop &other);
};
struct BinProp:Prop{
    Prop *p1, *p2;
    LogicType l;
    BinProp(){}
    BinProp(Prop* p1, LogicType l, Prop* p2):p1(p1), p2(p2), l(l){}
    bool operator==(Prop &other);
};
struct InequProp:Prop{
    Expr *e1, *e2;
    PropType p;
    bool operator==(Prop &other);
};
/*
struct QuantProp: Prop{
    Prop* p;
    vector<Expr*> v_e;
    QuantType t;
    bool operator==(Prop &other);
};*/
#endif
